本发明公开了一种列控系统通信协议规范化设计的方法,包括:根据列控系统的协议需求,制定列控系统协议的案例集合;绘制所述案例集合中的每个案例的顺序序列图;建立形式化协议模型;对建立的协议模型依次进行语义和语法验证、仿真和形式化验证,若在验证或仿真阶段出现问题,返回到建立协议模型的步骤进行重建或修改;最后形成模型库并生成协议模型分析报告。本发明还公开了一种列控系统通信协议规范化设计的系统。本发明通过按列控系统的协议需求,对系统协议进行建模,并对该模型进行验证,使得在协议设计过程中避免了二义性,及早地发现协议中的错误。
1.一种列控系统通信协议规范化设计的方法,其特征在于,包括以下步骤:S1:根据列控系统的协议需求,制定列控系统协议的案例集合;S2:采用消息序列图MSC引用场景方式来体现列控协议业务场景的先后顺序性,以绘制所述案例集合中的每个案例的顺序序列图;S3:以所述顺序序列图为出发点,建立模型输入输出原语集,划分协议系统模块与进程状态,设计并建立形式化协议模型;S4:对步骤S3中建立的所述形式化协议模型进行语义和语法验证,若通过验证,则执行步骤S5,否则,返回S3重新建立或修改所述形式化协议模型;S5:对通过验证后的所述形式化协议模型进行仿真,并根据仿真结果检查协议模型中是否存在不符合所述顺序序列图中的顺序,若存在,返回步骤S3重新建立或修改所述形式化协议模型,否则,执行步骤S6;S6:对仿真后的所述形式化协议模型进行形式化验证,检查协议的属性、符号覆盖率及所有行为树的行为路径,若通过验证,则执行步骤S7,否则,返回步骤S3重新建立或修改所述形式化协议模型;S7:形成模型库并生成协议模型分析报告。
2.如权利要求1所述的列控系统通信协议规范化设计的方法,其特征在于,所述输入输出原语集包括:独立原语集合,发起原语集合和跟随原语集合。
3.如权利要求1所述的列控系统通信协议规范化设计的方法,其特征在于,所述步骤S3中的形式化协议模型是基于进程状态机的模型。
4.一种列控系统通信协议规范化设计的系统,其特征在于,包括:案例集合制定模块,用于根据列控系统的协议需求,制定列控系统协议的案例集合;顺序序列图绘制模块,用于采用消息序列图MSC引用场景方式来体现列控协议业务场景的先后顺序性,以绘制所述案例集合中的每个案例的顺序序列图;协议模型建立模块,用于以所述顺序序列图为出发点,建立模型输入输出原语集,划分协议系统模块与进程状态,设计并建立形式化协议模型;语义和语法验证模块,用于对协议模型建立模块中所建立的所述形式化协议模型进行语义和语法验证,若通过验证,则执行仿真模块,否则,返回协议模型建立模块重新建立或修改所述形式化协议模型;仿真模块,用于对通过验证后的所述形式化协议模型进行仿真,并根据仿真结果检查协议模型中是否存在不符合所述顺序序列图中的顺序,若存在,返回协议模型建立模块重新建立或修改所述形式化协议模型,否则,执行形式化验证模块;形式化验证模块,用于对仿真后的所述形式化协议模型进行形式化验证,检查协议的属性、符号覆盖率及所有行为树的行为路径,若通过验证,则执行模型库生成模块,否则,返回协议模型建立模块重新建立或修改所述形式化协议模型;模型库生成模块,用于形成模型库并生成协议模型分析报告。技术领域
本发明涉及列控系统通信协议设计技术领域,特别涉及一种列控系统通信协议规范化开发的方法及系统。
背景技术
目前,随着我国轨道交通飞速发展,高速列车运行控制系统也进入了CTCS-3级时代,CTCS-3列车运行控制系统依赖于高容量传输系统进行数据传输,已完成高运行效率、高可靠的运行质量。而城市轨道交通也进行入基于通信的移动闭塞时代,其列车运行控制系统的数据传输也依赖于双向高容量的传输系统,很明显,基于通信的列车运行控制系统中的通信协议,应具有保证数据正常、有效、或安全传输功能,其在保障列车安全行车方面占有十分重要的地位。在以往的列车运行控制系统中,通信协议的功能以及机制往往是被忽视的,随着数据传输功能在列控系统的作用的日益重要,根据不同的传输环境存在着多种通信协议的现象。对于轨道交通的通信协议而言,从传输的对象分类,可以分为车地通信协议和地面通信协议。从安全性的角度,可以分为安全通信协议和非安全通信协议。针对列控系统的特点,通信协议往往是由不同的设备厂商生产开发,就存在一个协议的互连互通的过程,对通信协议的规范化说明及开发,明确通信协议的需求、功能、设计、实现过程,具有十分重要的意义。以往的列控系统协议开发方法中,一般采用采用自然语言描述的设计文档,以及直接的编码过程。这种开发过程对列控系统协议的描述存在着二义性特点,同时,其不能在早期发现设计错误,以及不能早期检查需求与设计是否完全一致。另外,对于列控系统中的安全协议设计,无法检查其设计的正确性以及高苛求性。
发明内容
(一)要解决的技术问题本发明要解决的技术问题是:如何在列控系统通信协议设计过程中避免对协议描述的二义性,以及能够在协议设计过程中及早地发现错误。(二)技术方案为解决上述技术问题,本发明提供了一种列控系统通信协议规范化设计的方法,包括以下步骤:S1:根据列控系统的协议需求,制定列控系统协议的案例集合;S2:采用消息序列图MSC(MESSAGExa0SEQUENCExa0CHART)引用场景方式来体现列控协议业务场景的先后顺序性,以绘制所述案例集合中的每个案例的顺序序列图;S3:以所述顺序序列图为出发点,建立模型输入输出原语集,划分协议系统模块与进程状态,设计并建立形式化协议模型;S4:对步骤S3中建立的所述形式化协议模型进行语义和语法验证,若通过验证,则执行步骤S5,否则,返回S3重新建立或修改所述形式化协议模型;S5:对通过验证后的所述形式化协议模型进行仿真,并根据仿真结果检查协议模型中是否存在不符合所述顺序序列图中的顺序,若存在,返回步骤S3重新建立或修改所述形式化协议模型,否则,执行步骤S6;S6:对仿真后的所述形式化协议模型进行形式化验证,检查协议的属性、符号覆盖率及所有行为树的行为路径,若通过验证,则执行步骤S7,否则,返回步骤S3重新建立或修改所述形式化协议模型;S7:形成模型库并生成协议模型分析报告。其中,所述输入输出原语集包括:独立原语集合,发起原语集合和跟随原语集合。其中,所述步骤S3中的形式化协议模型是基于进程状态机的模型。本发明还提供了一种列控系统通信协议规范化设计的系统,包括:案例集合制定模块,用于根据列控系统的协议需求,制定列控系统协议的案例集合;顺序序列图绘制模块,用于采用MSC引用场景方式来体现列控协议业务场景的先后顺序性,以绘制所述案例集合中的每个案例的顺序序列图;协议模型建立模块,用于以所述顺序序列图为出发点,建立模型输入输出原语集,划分协议系统模块与进程状态,设计并建立形式化协议模型;语义和语法验证模块,用于对协议模型建立模块中所建立的所述形式化协议模型进行语义和语法验证,若通过验证,则执行仿真模块,否则,返回协议模型建立模块重新建立或修改所述形式化协议模型;仿真模块,用于对通过验证后的所述形式化协议模型进行仿真,并根据仿真结果检查协议模型中是否存在不符合所述顺序序列图中的顺序,若存在,返回协议模型建立模块重新建立或修改所述形式化协议模型,否则,执行形式化验证模块;形式化验证模块,用于对仿真后的所述形式化协议模型进行形式化验证,检查协议的属性、符号覆盖率及所有行为树的行为路径,若通过验证,则执行模型库生成模块,否则,返回协议模型建立模块重新建立或修改所述形式化协议模型;模型库生成模块,用于形成模型库并生成协议模型分析报告。(三)有益效果本发明通过按列控系统的协议需求,对系统协议进行建模,并对该模型进行验证,使得在协议设计过程中避免了二义性,及早的发现协议中的错误。
附图说明
图1是本发明实施例的一种列控系统通信协议规范化设计的方法流程图;图2是本发明实施例的一种列控系统通信协议规范化设计的系统结构示意图。
具体实施方式
下面结合附图和实施例,对本发明的具体实施方式作进一步详细描述。以下实施例用于说明本发明,但不用来限制本发明的范围。如图1所示,为本发明实施例的列控系统通信协议规范化设计的方法流程图,包括:步骤S101,根据列控系统的协议需求,制定列控系统协议的案例集合。需求分析中,选定UML适用于列控通信协议系统的元素,形成基本的设计配置元素。UML中的选用元素为:用例图元素、类图元素、组件元素以及状态图元素,这些元素用于分析列控系统通信协议的软件结构、硬件结构和用例。其中,用例图表达列控系统中的各种协议场景,类图可表示在协议系统的对象关系,而组件图则表示实际系统的连接关系。步骤S102,绘制所述案例集合中的每个案例的顺序序列图。MSC语言为一种用来描述多个实体之间和实体与环境之间消息交互的顺序,在本实施例中使用其细化UML用例图中协议业务场景。在列控系统的通信协议中,往往一些业务场景都是具有先后顺序的,一般的,这种先后关系可采用MSC引用来表示。在需求管理中,用例图与MSC图之间的关系为“业务宏观图——>业务关系图”以及业务中信息交互顺序图,从这种图组合表示中,可以将某个协议的所有用例以及用例之间表示清楚。步骤S103,以顺序序列图为出发点,建立模型输入输出原语集,划分协议系统模块与进程状态,设计并建立形式化协议模型,即根据各案例的顺序序列图建立SDL形式化协议模型,具体为基于状态机的模型,具体地:(1)对形式化协议系统进行软件结构细分。(2)抽取MSC图的简单业务图中的实例,并对实例进行归类,最后形成的一类即为一个状态机进程。(3)确定状态机进程的调用过程。(4)根据业务行为图例。对输入输出进行筛选,形成输入输出集合,从而形成以输入为触发的状态集合。(5)状态机进程的具体设计,使用SDL规范描述语言进行描述,其所包含的元素:输入元素,状态元素、输出元素,以及进程元素等。根据步骤(4)中的状态集合以及输入输出集合,描述状态跃迁过程。细化输入输出参数以及具体的操作行为。步骤S104,对步骤S103中建立的协议模型进行语义和语法验证,若通过验证,则执行步骤S105,否则返回S103重新建立或修改协议模型。步骤S105,对验证后的协议模型进行仿真,并根据仿真结果检查协议模型中是否存在不符合所述顺序序列图中的顺序,若存在返回步骤S103重新建立或修改协议模型,否则执行步骤S106;步骤S106,对仿真后的协议模型进行形式化验证,检查协议的属性、符号覆盖率及所有行为树的行为路径。首先,先确认模型的执行是否与需求的业务过程一致,是否满足了需求,其次,通过对设计模型的遍历性验证,确保不存在错误的状态跃迁等安全隐患,保证协议设计模型的正确性。若通过验证,则执行步骤S107,否则返回步骤S103重新建立或修改协议模型;步骤S107,形成模型库并生成协议模型分析报告。针对列控系统中车地安全通信协议EuroRadio协议为例,对本发明方法进一步说明。步骤1,EuroRadio协议的需求按照其安全业务要求可分为:通道测试、注册过程、通信连接建立过程、数据传输过程、高级数据传输过程、通信连接注销过程。根据业务顺序关系,也可有EuroRadio协议业务整体顺序图。步骤2,绘制所述案例集合中的每个案例的顺序序列图,然后,确定输入输出原语,并进行分类,可分为独立原语集合,发起原语集合,跟随原语集合。独立原语集合包括:通道测试请求原语、通道测试指示原语、注册请求原语、注册指示原语等。发起原语集合:用户建链请求原语、用户建链确认原语、通信连接确认原语、通信数据请求原语、通信数据指示原语、用户数据传输请求原语、通信数据请求原语、数据传输指示原语、用户数据传输指示原语、用户建链终止请求原语、通信终止请求原语、通信终止指示原语、用户建链终止指示原语。跟随原语集合:用户建链响应原语、用户建链指示原语、通信连接指示原语、通信连接响应原语、通信数据指示原语、通信数据请求原语、用户数据传输请求原语、用户数据传输指示原语、用户建链终止请求原语、通信终止请求原语、通信终止指示原语、用户建链终止指示原语。步骤3,通过对EuroRadio协议的案例序列分析,将协议状态机分为三个有限状态机(亦可称为进程),分别为管理状态机,发起状态机、跟随状态机。具体的步骤如下:将输入原语分类,根据输入原语分类确定主进程以及次进程。子进程包括发起进程与跟随进程。主进程负责处理独立原语集合的输入输出原语,并负责对此次进程的创建以及删除,以及相应输入输出原语的管理。次进程主要针对本进程的状态管理以及维护,各种输入原语触发的状态变换以及对应输出。发起进程需要完成的业务有发起通信连接过程、数据传输过程、通信连接终止过程等。跟随进程需要完成的业务有跟随通信连接过程、数据传输过程、通信连接终止过程。步骤4,在有了基本的EuroRadio协议模型之后,需要进行语义语法检查,一般的,需要确定模块的所包括的进程、输入输出原语,检查输入输出原语与各级模块、各自进程之间的对应关系。若通过验证,则执行步骤5,否则返回步骤3重新建立或修改状态机协议模型。步骤5,对主进程、发起进程、跟随进程与步骤1之间的需求满足确认,在本设计中,进程中包含了多个业务关系,需对各个进程按照业务关系以及顺序进行仿真,以确认模型是否与需求的业务关系一致。若存在返回步骤3重新建立或修改状态机协议模型,否则执行步骤6。由于本设计中分为发起进程与跟随进程,一般的,须对该进程进行双向确认仿真,例如,发起进程中的通信连接仿真过程只可以模拟通信连接建立过程的发起方一方的行为。跟随进程中的通信连接仿真过程只可以模拟通信连接建立过程的跟随方一方的行为。步骤6,通常对模型的状态机的形式化验证过程,是对状态空间的一个遍历过程,在本平台中,对EuroRadio协议的考核标准为是否有死锁、活锁、状态不可达等。若通过验证,则执行步骤7,否则返回步骤3重新建立或修改状态机协议模型。步骤7,形成模型库并生成协议模型分析报告。本发明还提出了一种列控系统通信协议规范化设计的系统,如图2所示,包括:案例集合制定模块,用于根据列控系统的协议需求,制定列控系统协议的案例集合;顺序序列图绘制模块,用于绘制所述案例集合中的每个案例的顺序序列图;协议模型建立模块,用于以所述顺序序列图为出发点,建立模型输入输出原语集,划分协议系统模块与进程状态机,设计并建立形式化协议模型;语义和语法验证模块,用于对协议模型建立模块中所建立的所述形式化协议模型进行语义和语法验证,若通过验证,则执行仿真模块,否则,返回协议模型建立模块重新建立或修改所述形式化协议模型;仿真模块,用于对通过验证后的所述形式化协议模型进行仿真,并根据仿真结果检查协议模型中是否存在不符合所述顺序序列图中的顺序,若存在,返回协议模型建立模块重新建立或修改所述形式化协议模型,否则,执行形式化验证模块;形式化验证模块,用于对仿真后的所述形式化协议模型进行形式化验证,检查协议的属性、符号覆盖率及所有行为树的行为路径,若通过验证,则执行模型库生成模块,否则,返回协议模型建立模块重新建立或修改所述形式化协议模型;模型库生成模块,用于形成模型库并生成协议模型分析报告。以上实施方式仅用于说明本发明,而并非对本发明的限制,有关技术领域的普通技术人员,在不脱离本发明的精神和范围的情况下,还可以做出各种变化和变型,因此所有等同的技术方案也属于本发明的范畴,本发明的专利保护范围应由权利要求限定。